k:Knd, T,B:Type, l:IdLnk, ds:fpf(Id; x.Type), tg:Id, f:(decl-state(ds)TB).
((isrcv(k))
 ((destination(lnk(k)) = source(l)  Id)  ((lnk(k) = l)  ((T = B)  (tag(k) = tg)))))
 normal-ds{i:l}
 normal-ds(ds)
 normal-type{i:l}
 normal-type(T)
 normal-type{i:l}
 normal-type(B)
 R-realizes{i:l}
 R-realizes(Rsends(ds; k; T; l; fpf-single(tg; B); cons(<tg, s,v. cons((f(s,v)); [])>; []));
 R-realizes(es.usends1-p(es;ds;k;T;l;tg;B;f)) 

latex

Definitions

es-state(es; i), decl-state(ds), False, A, A  B, ge(i; j), Y, ||as||, t.2, fpf-ap(f; eq; x), fpf-single(x; v), ff, tt, if b then t else f fi , fpf-cap(f; eq; x; z), P  Q, P  Q, x:A. B(x), alle-at(es; i; e.P(e)), A c B, usends1-p(es;ds;k;T;l;tg;B;f), x. t(x), prop{i:l}, guard(T), sq_type(T), top, decl-type{i:l}(ds; x), t  T, P  Q, P  Q, x:A. B(x), hd(l), Unit, , es-rcv-from(es; e; l; L), t.1, append(as; bs), reduce(f; k; as), sends-msgs(s; v; tg_f), concat(ll), map(f; as), sends-p(es; ds; k; T; l; dt; g), x(s),

Lemmas

non neg length, es-lnk wf, length-map, es-vartype wf, subtype rel dep function, es-state-when wf, es-val wf, hd wf, pi2 wf, assert of bnot, eqff to assert, not wf, bnot wf, iff transitivity, eqtt to assert, bool wf, top wf, fpf-single wf, fpf-dom wf, subtype rel self, subtype rel product, subtype rel list, equal functionality wrt subtype rel, es-isrcv wf, l member wf, iff functionality wrt iff, es-tag wf, fpf-single-dom, es-rcv-kind, es-sender wf, member singleton, length wf1, rcv wf, es-kind-rcv, es-E wf, es-loc wf, es-kind wf, usends1-p wf, event system wf, fpf-cap wf, sends-p wf, Rsends wf, R-implies-rule, Knd wf, fpf wf, decl-state wf, tagof wf, IdLnk wf, lsrc wf, ldst wf, Id wf, isrcv wf, normal-ds wf, normal-type wf, normal-ds-single, eq lnk wf, assert wf, Id sq, lnk wf, assert-eq-lnk, decl-type wf, id-deq wf, fpf-cap-single1, R-sends-rule, fpf-single wf3